\newcommand{\app}[2]{{#1}\langle{#2}\rangle}
We now %have 
examine the impact on decidability of bisimilarity of %a few
some extensions of \ahopi. %For lack of space we 
We omit the details, including precise statements  of the results. 

%\iflong{
\paragraph{Abstractions.}
%}{\noindent{\bf Abstractions.}}
%\iflong{
An {\em abstraction} is an
 expression of the form $(x)  P$; it
 is a
 parametrized process.
An abstraction  has a {functional} type.  
Applying an  abstraction $( x) P$ of type $T \rightarrow \behtype $ (where $
\behtype$ is the type of all processes)  to an  argument $W$ of 
 type $T$  yields the  process $P \sub W x$. The argument $W$  can itself  be an
 abstraction; therefore the order of an abstraction, that is, the level 
 of arrow nesting in its type, can be arbitrarily high. The order can
 also be $\omega$, if there are recursive types.
By setting bounds on the order of the types of  abstractions, one can define 
a hierarchy of subcalculi of the Higher-Order $\pi$-calculus \citep{SaWabook}; and when
this bound is $\omega$, one obtains a calculus capable of representing
the $\pi$-calculus (for this all operators of the Higher-Order
$\pi$-calculus are needed, including full restriction).

Allowing the communication of abstractions, as in the Higher-Order
$\pi$-calculus, one then also needs 
to add in the grammar for processes an {\em application} construct of the form 
$P_1 \angp{P_2}$, as a destructor for abstractions.
Extensions in the LTS would be as follows.
Suppose, as in \citep{San96int}, that {\em beta-conversion} $\succ$ is the least precongruence on \ahopi processes
generated by the rule
\[
(x)P_1 \angp{P_2} \succ P_1 \sub {P_2} x.
\]
The LTS could be then extended with a rule 
\infrule{\textsc{Beta}~~}{P \succ P_1' \andalso 
P_1' \arr \alpha Q }{P \arr \alpha Q}
Notice that with these additions, the characterization of bisimilarity as IO bisimilarity
still holds. 
For a \ahopi extended with abstractions and applications, 
$\simIOo$ is still a congruence and is preserved by substitutions (by 
straighforward extensions of the proofs of Lemmas \ref{l:simIOo_cong} 
and \ref{l:simIOo_sub}).
Note that, however, abstraction application may increase the size of processes.
If abstractions are of finite type (i.e., their order is smaller than $\omega$) then only a finite number of
such applications is possible, and decidability of bisimilarity is preserved. 
%Decidability of bisimilarity is maintained as long as abstractions of finite type 
%(i.e., order smaller than $\omega$) are considered. 
Decidability fails if the order is $\omega$, intuitively because in
this case it is possible to simulate the $\lambda$-calculus. 
% }{
% An abstraction is a parametrized process
% of the form $(x)  P$ that has a {functional} type $T \rightarrow T'$.  
% Applying an  abstraction $( x) P$ 
% to an  argument $W$ 
% yields the  process $P \sub W x$. Since $W$  can itself  be an
%  abstraction, the {\em order} of an abstraction
% ---the level of arrow nesting in its type--- can be arbitrarily high 
% (even $\omega$, if there are recursive types).
% Allowing the exchange of abstractions, as in the Higher-Order
% $\pi$-calculus, requires an application construct, as a 
% destructor for abstractions. 
% By setting bounds on the order of  abstractions, one can define 
% a hierarchy of subcalculi of the Higher-Order $\pi$-calculus \cite{SaWabook}; and when
% this bound is $\omega$, one obtains a calculus able to represent
% the $\pi$-calculus (all operators of the Higher-Order
% $\pi$-calculus are needed, including full restriction).
% 
% We have proved that extending \ahopi with abstractions of order smaller than $\omega$
% maintains the decidability of bisimilarity. 
% Decidability then fails if the $\omega$ bound is removed, intuitively because in
% this case it is possible to simulate the $\lambda$-calculus. }

\iflong{
\paragraph{Output prefix}
If we add an output prefix construct $\out a P. Q$ to \ahopi, then the
proof of the characterization as  IO bisimilarity    breaks and, with it, 
 the proof of  decidability.  Decidability proofs can however be adjusted 
by appealing to results on unique decomposition of processes and axiomatization (along the lines of Section~\ref{s:axiom}).

}{%\noindent{\bf Output prefix.} 
%If we add an output prefix construct $\out a P. Q$ to \ahopi, then the
%proof of the characterization as  IO bisimilarity    breaks and, with it, 
% the proof of  decidability.  Decidability proofs can however be adjusted 
%by appealing to results on unique decomposition of processes and axiomatization (along the lines of Section~\ref{s:axiom}).
%In short, all results in 
%Sections \ref{s:bism}--\ref{s:axiom} remain valid, but the proofs 
%need a substantial revision and become more complex. 
}

%\iflong{
\paragraph{Choice.}
%}{\noindent{\bf Choice.} }
Decidability remains with the addition of a choice operator to \ahopi.
%\finish{input-guarded choice?}
%Little modifications are needed in the proofs. 
The proofs require little modifications. 
The addition of both choice and output prefix is harder.
It might be possible to extend  the decidability proof for output prefix mentioned
above so to accommodate also choice, but 
%we have not checked all
the details %, which 
become much more complex.  


%\iflong{
\paragraph{Recursion.}
%}{\noindent{\bf Recursion.}}
We do not know whether decidability is maintained by the addition of
recursion (or similar operators such as replication).  
